from deslab import fsa, ac ,coac, syms, EMPTYSET, draw, UNDEFINED
from deslab import strconncomps,selfloopnodes
import networkx as nx
LIMIT_DIAGNOSER = 100000

"""This is the toolbox for failure diagnosis. It contains algorithms
for building a diagnoser a verifier and to test diagnosability
 """


def observer(self, Sigma_o=UNDEFINED):    
    """ This function calculates a deterministic automaton
    which marks and generates the projection of the marked and
    generated languages of the input automaton G over the alphabet
    of observable events Sigma_o, defined by the user. If a list (or set)
    of observable events is not provided, the function observer takes
    the set Sigobs of the input automaton as the set of observable
    events"""

    # inner functions    
    def Gamma_obs(set): # Gamma observer calcularion                        
        active_events = EMPTYSET
        for q in set:
            active_events = active_events | self.Gamma(q)
        active_events = active_events & Sigma_obs
        return active_events  

    # Main program    
    # easy name for parameters
    X0, X = self.X0, self.X
    Sigma, Xm, Sigobs = self.Sigma, self.Xm, self.Sigobs    
    # determinig the set of  unobservable events
    if (Sigma_o == UNDEFINED) : # Sigma_o was not defined
        Sigma_obs = Sigobs
        Sigma_uobs = Sigma - Sigobs        
    elif isinstance(Sigma_o,list) | isinstance(Sigma_o,set):      
        Sigma_obs = frozenset(Sigma_o)
        Sigma_uobs = Sigma - Sigma_obs         
    elif isinstance(Sigma_o,frozenset):
        Sigma_obs = Sigma_o 
        Sigma_uobs = Sigma - Sigma_o
    else: 
        raise invalidArgument, 'Observed set must be of type set, frozenset or list'        
    # in the case of not observable events
    # we return the input automaton         
    if (self.is_dfa() &  (Sigma_obs == self.Sigma)):
        return self       
    #initial values of parameters
    X0_obs = self.unobsreach(X0,Sigma_obs)    
    X_obs = [X0_obs]
    S = [X0_obs] # unobs. reach of X0 as initial value of stack
    transition = []
    Xm_obs = []  
    complete=True 
    # updating X0_p label
    # testing of X0obs is marked
    if X0_obs & Xm <> EMPTYSET: 
        Xm_obs.append(X0_obs)
    # main stack cycle      
    while S <> []: # beginning of subset construction      
        Q = S.pop()                     
        for sigma in Gamma_obs(Q):
            Q_next = self.deltaobs(Q,sigma,Sigma_obs) # reached set 
            if Q_next not in X_obs: # net state found
                X_obs.append(Q_next)
                if len(X_obs) > LIMIT_DIAGNOSER:
                    complete = False
                    break
                S.append(Q_next) 
                if Q_next & Xm <> EMPTYSET: # marking that state
                    Xm_obs.append(Q_next) 
            transition.append([Q,sigma,Q_next])

    # defining the observer DFA           
    observer = fsa(X_obs, Sigma_obs, transition, [X0_obs],
                   Xm_obs, Sigobs = Sigma_obs, name=complete) 
    return observer 


def labelfailaut(sf):
    """
    This function creates a label failure automaton in 
    the context of failure diagnosis
    """
    # first we check if input parameters were correctly passed
    if isinstance(sf, list):
        sf = sf[0]
    elif isinstance(sf,set):
        sf = list(sf)[0]
    elif isinstance(sf,frozenset):
        sf = list(sf)[0]     
    elif isinstance(sf,str):
        pass   
    else:
        raise invalidArgument, 'sf must be string, list or set'
     
    Y,N = syms('Y N')
    sigmaA = [sf]
    XA = [Y,N]
    X0A = [N]
    XmA = []
    T = [(N,sf,Y),(Y,sf,Y)]
    Al=fsa(XA,sigmaA,T,X0A,XmA, Sigobs=EMPTYSET, name='Al')
    return Al



def is_diagnosable_verif(G, sf, Sigma_o=UNDEFINED):
    """ This function implements the verifier proposed by Basilio
    and Moreira """
    
    # first we check if input parameters were correctly passed
    if isinstance(sf, list):
        sf = sf[0]
    elif isinstance(sf,set):
        sf = list(sf)[0]
    elif isinstance(sf,frozenset):
        sf = list(sf)[0]  
    elif isinstance(sf, str):
        pass      
    else:
        raise invalidArgument, 'sf must be string, list or set'
    # now we check the input parameter
    if (Sigma_o == UNDEFINED) : # Sigma_o was not defined
        Sigma_obs = G.Sigobs     
    elif isinstance(Sigma_o,list) | isinstance(Sigma_o,set):      
        Sigma_obs = frozenset(Sigma_o)                
    elif isinstance(Sigma_o, frozenset):
        Sigma_obs = Sigma_o     
    else:
       raise invalidArgument, 'Observed set must be of type set or list'   
    # STEP 1   
    Sigma_uo = G.Sigma - Sigma_obs    
    GN_prime = G.deletevent(sf)    
    GN = ac(GN_prime)    
    # STEP 2
    Al = labelfailaut(sf)
    Gl = G//Al
    Xml = [(x,l) for (x,l) in Gl.X if l=='Y'] 
    Gl = Gl.setpar(Xm=Xml)
    GY = coac(Gl)
    R = [(event,event+'_R') for event in Sigma_uo]
    GN = GN.renamevents(R)
    GV = GN//GY
    XmV = [(xN,(xY,l)) for (xN,(xY,l)) in GV.X if l=='Y']
    GV = GV.setpar(Xm=XmV)   
    try:
        SCC_selfloop = [[l] for l in selfloopnodes(GV)]
    except:
        draw(GV,GY,GN)
    SCC_multiple = [C for C in strconncomps(GV) if (len(C)>1)]
    SCC_nontrivial = SCC_selfloop + SCC_multiple
    diagnosable = True
    # finding a counter example
    for C in SCC_nontrivial:
        for x_V in (set(C) & GV.Xm):
            if (GV.Gamma(x_V) & G.Sigma) <> set([]):
                diagnosable = False
                break
    return diagnosable, GV



def diagnoser(G, sf, Sigma_o=UNDEFINED):
    """Function that builds and renders an event Diagnoser
    based on theoretical concepts of Sampath and Lafortune"""
    # first we check if input parameters were correctly passed
    if isinstance(sf, list):
        sf = sf[0]
    elif isinstance(sf,set):
        sf = list(sf)[0]
    elif isinstance(sf,frozenset):
        sf = list(sf)[0] 
    elif isinstance(sf, str):
        pass       
    else:
        raise invalidArgument, 'sf must be string, list or set'
    # we can use the inner observable events for diagnoser computation
    # or the set of observable events passed by the user 
    if (Sigma_o == UNDEFINED) : # Sigma_o was not defined
        Sigma_obs = G.Sigobs     
    elif isinstance(Sigma_o,list) | isinstance(Sigma_o,set):      
        Sigma_obs = frozenset(Sigma_o)                
    elif isinstance(Sigma_o, frozenset):
        Sigma_obs = Sigma_o     
    else:
       raise invalidArgument, 'Observed set must be of type set or list'   
    # we render the automaton using accepted notation
    A = labelfailaut(sf)  
    D = observer(G//A, Sigma_obs)      
    D.setgraphic('diagnoser')                   
    return D



def is_diagnosable_diag(G, sf, Sigma_o= UNDEFINED ):   
    """This function looks for indeterminate states, i. e.
    states that belong to indeterminate  SCCs    
     """ 
    if isinstance(sf, list):
        sf = sf[0]
    elif isinstance(sf,set):
        sf = list(sf)[0]
    elif isinstance(sf,frozenset):
        sf = list(sf)[0] 
    elif isinstance(sf, str):
        pass       
    else:
        raise invalidArgument, 'sf must be string, list or set'
    # we can use the inner observable events for diagnoser computation
    # or the set of observable events passed by the user 
    if (Sigma_o == UNDEFINED) : # Sigma_o was not defined
        Sigma_obs = G.Sigobs     
    elif isinstance(Sigma_o,list) | isinstance(Sigma_o,set):      
        Sigma_obs = frozenset(Sigma_o)                
    elif isinstance(Sigma_o, frozenset):
        Sigma_obs = Sigma_o     
    else:
       raise invalidArgument, 'Observed set must be of type set or list'              
    # Calculating the labeling plant  
    Gd = diagnoser(G, sf, Sigma_obs)  
    if Gd.name == False:
        return False, Gd           
    A = labelfailaut(sf) 
    Gl = G//A  # G_l
    # Calculating diagnoser
   
    Gt= Gd//Gl   
    SCC = strconncomps(Gt)      
    SCC_selfloop = [[l] for l in selfloopnodes(Gt)]
    SCC_multiple = [C for C in SCC if (len(C)>1)]
    SCC_nontrivial = SCC_selfloop + SCC_multiple
    diagnosable = True
    for C in SCC_nontrivial:
        if any(l=='Y' and YN_type(xd)=='YN'  for xd, (x,l) in C):
            diagnosable = False
            break                       
    return diagnosable, Gd



def YN_type(xd):
    """Determines if a diagnoser state is a faulty, normal
    or uncertain state"""
    if all(l=='Y' for x,l in xd):
        return 'Y'
    elif all(l=='N' for x,l in xd):
        return 'N'        
    else:
        return 'YN'


def rename_diagnoser(Gd):
    map=[]    
    for i, xd in enumerate(Gd.X):   
    
        if all(l=='Y' for x,l in xd):
            map.append((xd, (i,'Y')))
        elif all(l=='N' for x,l in xd):
            map.append((xd, (i,'N')))
        else:
            map.append((xd,(i,'YN')))          
    Gdren = Gd.renamestates(map)
    Gdren.name = Gd.name     
    return Gdren


def nonobservable_scc(G):
    T_f = [(t[0],t[2]) for t in G.transitions_iter() if t[1] in G.Sigma-G.Sigobs]
    F = nx.MultiDiGraph(T_f)
    SCC = strconncomps(F)      
    SCC_selfloop = [[l] for l in selfloopnodes(F)]
    SCC_multiple = [C for C in SCC if (len(C)>1)]
    SCC_nontrivial = SCC_selfloop + SCC_multiple
    return SCC_nontrivial


def nonobservable_fail_scc(G,sf):
    T_f = [(t[0],t[2]) for t in G.transitions_iter() if t[1] in G.Sigma-G.Sigobs]
    F = nx.MultiDiGraph(T_f)
    SCC = strconncomps(F)      
    SCC_selfloop = [[l] for l in selfloopnodes(F)]
    SCC_multiple = [C for C in SCC if (len(C)>1)]
    SCC_nontrivial = SCC_selfloop + SCC_multiple
    for C in SCC_nontrivial:
        for x in C:
            if sf in G.Gamma(x):
                if G.delta(x,sf) in C:
                    return False, F.size()
                                     
    return True, F.size()

#def dfs(H, source=None):
#    """Produce edges in a depth-first-search starting at source.
#"""
#    nodes=list(source)
#    visited=set()
#    for start in nodes:
#        if start in visited:
#            continue
#        visited |= set([start])
#        stack = [(start,iter(G[start]))]
#        while stack:
#            parent,children = stack[-1]
#            try:
#                child = next(children)
#                if child not in visited:                    
#                    visited |= set([child])                    
#                    stack.append((child,iter(G[child])))
#            except StopIteration:
#                stack.pop()
#    visited = frozenset(visited)
#    return visited



